Skip to content

Instantly share code, notes, and snippets.

@botic

botic/bsp7.c

Created November 21, 2011 14:41
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save botic/1382794 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save botic/1382794 to your computer and use it in GitHub Desktop.
Download ZIP
FMI Beispiel 7 – CMBC
Raw
bsp7.c
void __CPROVER_assert (int, char*);
int nondet_int ();
#define TRUE 1
#define FALSE 0
#define NUM_PROFESSORS 5
#define NUM_COURSES 4
int main (int argc, char* argv[])
{
int prof_to_courses [NUM_PROFESSORS][NUM_COURSES] =
{
{TRUE, FALSE, TRUE, FALSE}, // Prof 0
{TRUE, FALSE, TRUE, FALSE}, // Prof 1
{FALSE, TRUE, FALSE, TRUE}, // Prof 2
{TRUE, FALSE, FALSE, TRUE}, // Prof 3
{FALSE, FALSE, FALSE, FALSE} // Prof 4
};
int i;
int guess [NUM_COURSES];
for (i = 0; i < NUM_COURSES; i++)
{
guess [i] = nondet_int();
}
// Check if professor in the solution teaches the course
int valid_course_prof_assignment = TRUE;
for (i = 0; i < NUM_COURSES; i++)
{
int prof = guess [i];
if (prof < 0 || prof >= NUM_PROFESSORS || prof_to_courses [prof][i] == FALSE)
{
valid_course_prof_assignment = FALSE;
}
}
// Check if prof only teaches one course per term
for (i = 0; i < NUM_PROFESSORS; i++)
{
int teaching = 0;
int u;
for (u = 0; u < NUM_COURSES; u++)
{
// if course's teacher match the current one
if (guess [u] == i)
{
teaching++;
}
}
// more than one course assignment for the current professor
if (teaching > 1)
{
valid_course_prof_assignment = FALSE;
}
}
// assert a found counterexample
__CPROVER_assert (!valid_course_prof_assignment, "Found a valid assignment!");
return (0);
}
Raw
cmbc-output.txt
file bsp7.c: Parsing
Converting
Type-checking bsp7
Generating GOTO Program
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Unwinding loop c::main.0 iteration 1 file bsp7.c line 25 function main
Unwinding loop c::main.0 iteration 2 file bsp7.c line 25 function main
Unwinding loop c::main.0 iteration 3 file bsp7.c line 25 function main
Unwinding loop c::main.0 iteration 4 file bsp7.c line 25 function main
Unwinding loop c::main.1 iteration 1 file bsp7.c line 35 function main
Unwinding loop c::main.1 iteration 2 file bsp7.c line 35 function main
Unwinding loop c::main.1 iteration 3 file bsp7.c line 35 function main
Unwinding loop c::main.1 iteration 4 file bsp7.c line 35 function main
Unwinding loop c::main.2 iteration 1 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 2 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 3 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 4 file bsp7.c line 52 function main
Unwinding loop c::main.3 iteration 1 file bsp7.c line 48 function main
Unwinding loop c::main.2 iteration 1 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 2 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 3 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 4 file bsp7.c line 52 function main
Unwinding loop c::main.3 iteration 2 file bsp7.c line 48 function main
Unwinding loop c::main.2 iteration 1 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 2 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 3 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 4 file bsp7.c line 52 function main
Unwinding loop c::main.3 iteration 3 file bsp7.c line 48 function main
Unwinding loop c::main.2 iteration 1 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 2 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 3 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 4 file bsp7.c line 52 function main
Unwinding loop c::main.3 iteration 4 file bsp7.c line 48 function main
Unwinding loop c::main.2 iteration 1 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 2 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 3 file bsp7.c line 52 function main
Unwinding loop c::main.2 iteration 4 file bsp7.c line 52 function main
Unwinding loop c::main.3 iteration 5 file bsp7.c line 48 function main
size of program expression: 336 assignments
simple slicing removed 1 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
Running propositional reduction
Solving with MiniSAT2 without simplifier
3239 variables, 10105 clauses
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 0.029s
Building error trace
Counterexample:
State 2 file /usr/include/stdlib.h line 134 thread 0
----------------------------------------------------
__mb_cur_max=0 (00000000000000000000000000000000)
State 3 file <built-in> line 20 thread 0
----------------------------------------------------
__CPROVER_memory=(assignment removed)
State 4 file <built-in> line 22 thread 0
----------------------------------------------------
__CPROVER_deallocated=NULL
State 5 file <built-in> line 23 thread 0
----------------------------------------------------
__CPROVER_bounds_check=NULL
State 6 file <built-in> line 24 thread 0
----------------------------------------------------
__CPROVER_malloc_size=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 7 file <built-in> line 25 thread 0
----------------------------------------------------
__CPROVER_alloc=(assignment removed)
State 8 file <built-in> line 26 thread 0
----------------------------------------------------
__CPROVER_alloc_size=(assignment removed)
State 9 file <built-in> line 35 thread 0
----------------------------------------------------
__CPROVER_rounding_mode=0 (00000000000000000000000000000000)
State 10 file /usr/include/stdlib.h line 337 thread 0
----------------------------------------------------
suboptarg=NULL
State 11 file /usr/include/stdio.h line 167 thread 0
----------------------------------------------------
__stdinp=NULL
State 12 file /usr/include/stdio.h line 168 thread 0
----------------------------------------------------
__stdoutp=NULL
State 13 file /usr/include/stdio.h line 169 thread 0
----------------------------------------------------
__stderrp=NULL
State 14 file /usr/include/stdio.h line 277 thread 0
----------------------------------------------------
sys_nerr=0 (00000000000000000000000000000000)
State 17 thread 0
----------------------------------------------------
c::argv'=(assignment removed)
State 21 file bsp7.c line 14 function main thread 0
----------------------------------------------------
bsp7::main::1::prof_to_courses={ { 1, 0, 1, 0 }, { 1, 0, 1, 0 }, { 0, 1, 0, 1 }, { 1, 0, 0, 1 }, { 0, 0, 0, 0 } } ({ { 00000000000000000000000000000001, 00000000000000000000000000000000, 00000000000000000000000000000001, 00000000000000000000000000000000 }, { 00000000000000000000000000000001, 00000000000000000000000000000000, 00000000000000000000000000000001, 00000000000000000000000000000000 }, { 00000000000000000000000000000000, 00000000000000000000000000000001, 00000000000000000000000000000000, 00000000000000000000000000000001 }, { 00000000000000000000000000000001, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000001 }, { 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 } })
State 22 file bsp7.c line 25 function main thread 0
----------------------------------------------------
bsp7::main::1::i=0 (00000000000000000000000000000000)
State 24 file bsp7.c line 27 function main thread 0
----------------------------------------------------
bsp7::main::1::guess={ 1, 0, 0, 0 } ({ 00000000000000000000000000000001, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 })
State 25 file bsp7.c line 25 function main thread 0
----------------------------------------------------
bsp7::main::1::i=1 (00000000000000000000000000000001)
State 28 file bsp7.c line 27 function main thread 0
----------------------------------------------------
bsp7::main::1::guess={ 1, 2, 0, 0 } ({ 00000000000000000000000000000001, 00000000000000000000000000000010, 00000000000000000000000000000000, 00000000000000000000000000000000 })
State 29 file bsp7.c line 25 function main thread 0
----------------------------------------------------
bsp7::main::1::i=2 (00000000000000000000000000000010)
State 32 file bsp7.c line 27 function main thread 0
----------------------------------------------------
bsp7::main::1::guess={ 1, 2, 0, 0 } ({ 00000000000000000000000000000001, 00000000000000000000000000000010, 00000000000000000000000000000000, 00000000000000000000000000000000 })
State 33 file bsp7.c line 25 function main thread 0
----------------------------------------------------
bsp7::main::1::i=3 (00000000000000000000000000000011)
State 36 file bsp7.c line 27 function main thread 0
----------------------------------------------------
bsp7::main::1::guess={ 1, 2, 0, 3 } ({ 00000000000000000000000000000001, 00000000000000000000000000000010, 00000000000000000000000000000000, 00000000000000000000000000000011 })
State 37 file bsp7.c line 25 function main thread 0
----------------------------------------------------
bsp7::main::1::i=4 (00000000000000000000000000000100)
State 40 file bsp7.c line 32 function main thread 0
----------------------------------------------------
bsp7::main::1::valid_course_prof_assignment=1 (00000000000000000000000000000001)
State 41 file bsp7.c line 35 function main thread 0
----------------------------------------------------
bsp7::main::1::i=0 (00000000000000000000000000000000)
State 43 file bsp7.c line 37 function main thread 0
----------------------------------------------------
bsp7::main::1::2::prof=1 (00000000000000000000000000000001)
Checking if Prof 1 is valid for course 0
State 47 file bsp7.c line 35 function main thread 0
----------------------------------------------------
bsp7::main::1::i=1 (00000000000000000000000000000001)
State 50 file bsp7.c line 37 function main thread 0
----------------------------------------------------
bsp7::main::1::2::prof=2 (00000000000000000000000000000010)
Checking if Prof 2 is valid for course 1
State 54 file bsp7.c line 35 function main thread 0
----------------------------------------------------
bsp7::main::1::i=2 (00000000000000000000000000000010)
State 57 file bsp7.c line 37 function main thread 0
----------------------------------------------------
bsp7::main::1::2::prof=0 (00000000000000000000000000000000)
Checking if Prof 0 is valid for course 2
State 61 file bsp7.c line 35 function main thread 0
----------------------------------------------------
bsp7::main::1::i=3 (00000000000000000000000000000011)
State 64 file bsp7.c line 37 function main thread 0
----------------------------------------------------
bsp7::main::1::2::prof=3 (00000000000000000000000000000011)
Checking if Prof 3 is valid for course 3
State 68 file bsp7.c line 35 function main thread 0
----------------------------------------------------
bsp7::main::1::i=4 (00000000000000000000000000000100)
State 71 file bsp7.c line 48 function main thread 0
----------------------------------------------------
bsp7::main::1::i=0 (00000000000000000000000000000000)
State 73 file bsp7.c line 50 function main thread 0
----------------------------------------------------
bsp7::main::1::3::teaching=0 (00000000000000000000000000000000)
State 74 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=0 (00000000000000000000000000000000)
State 78 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=1 (00000000000000000000000000000001)
State 83 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=2 (00000000000000000000000000000010)
State 87 file bsp7.c line 57 function main thread 0
----------------------------------------------------
bsp7::main::1::3::teaching=1 (00000000000000000000000000000001)
State 88 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=3 (00000000000000000000000000000011)
State 93 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=4 (00000000000000000000000000000100)
State 98 file bsp7.c line 48 function main thread 0
----------------------------------------------------
bsp7::main::1::i=1 (00000000000000000000000000000001)
State 101 file bsp7.c line 50 function main thread 0
----------------------------------------------------
bsp7::main::1::3::teaching=0 (00000000000000000000000000000000)
State 102 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=0 (00000000000000000000000000000000)
State 105 file bsp7.c line 57 function main thread 0
----------------------------------------------------
bsp7::main::1::3::teaching=1 (00000000000000000000000000000001)
State 106 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=1 (00000000000000000000000000000001)
State 111 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=2 (00000000000000000000000000000010)
State 116 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=3 (00000000000000000000000000000011)
State 121 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=4 (00000000000000000000000000000100)
State 126 file bsp7.c line 48 function main thread 0
----------------------------------------------------
bsp7::main::1::i=2 (00000000000000000000000000000010)
State 129 file bsp7.c line 50 function main thread 0
----------------------------------------------------
bsp7::main::1::3::teaching=0 (00000000000000000000000000000000)
State 130 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=0 (00000000000000000000000000000000)
State 134 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=1 (00000000000000000000000000000001)
State 138 file bsp7.c line 57 function main thread 0
----------------------------------------------------
bsp7::main::1::3::teaching=1 (00000000000000000000000000000001)
State 139 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=2 (00000000000000000000000000000010)
State 144 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=3 (00000000000000000000000000000011)
State 149 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=4 (00000000000000000000000000000100)
State 154 file bsp7.c line 48 function main thread 0
----------------------------------------------------
bsp7::main::1::i=3 (00000000000000000000000000000011)
State 157 file bsp7.c line 50 function main thread 0
----------------------------------------------------
bsp7::main::1::3::teaching=0 (00000000000000000000000000000000)
State 158 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=0 (00000000000000000000000000000000)
State 162 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=1 (00000000000000000000000000000001)
State 167 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=2 (00000000000000000000000000000010)
State 172 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=3 (00000000000000000000000000000011)
State 176 file bsp7.c line 57 function main thread 0
----------------------------------------------------
bsp7::main::1::3::teaching=1 (00000000000000000000000000000001)
State 177 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=4 (00000000000000000000000000000100)
State 182 file bsp7.c line 48 function main thread 0
----------------------------------------------------
bsp7::main::1::i=4 (00000000000000000000000000000100)
State 185 file bsp7.c line 50 function main thread 0
----------------------------------------------------
bsp7::main::1::3::teaching=0 (00000000000000000000000000000000)
State 186 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=0 (00000000000000000000000000000000)
State 190 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=1 (00000000000000000000000000000001)
State 195 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=2 (00000000000000000000000000000010)
State 200 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=3 (00000000000000000000000000000011)
State 205 file bsp7.c line 52 function main thread 0
----------------------------------------------------
bsp7::main::1::3::u=4 (00000000000000000000000000000100)
State 210 file bsp7.c line 48 function main thread 0
----------------------------------------------------
bsp7::main::1::i=5 (00000000000000000000000000000101)
Assignment: 1
Violated property:
file bsp7.c line 70 function main
Found a valid assignment!
!(_Bool)valid_course_prof_assignment
VERIFICATION FAILED
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment