On Wed, Jun 14, 2017 at 9:53 AM, Vlastimil Babka <vbabka@xxxxxxx> wrote: > On 06/14/2017 01:08 AM, Dan Williams wrote: >> Turn the macro into a static inline and rewrite the condition checks for >> better readability in preparation for adding another condition. >> >> Cc: Jan Kara <jack@xxxxxxx> >> Cc: Andrew Morton <akpm@xxxxxxxxxxxxxxxxxxxx> >> Reviewed-by: Ross Zwisler <ross.zwisler@xxxxxxxxxxxxxxx> >> [ross: fix logic to make conversion equivalent] >> Acked-by: "Kirill A. Shutemov" <kirill.shutemov@xxxxxxxxxxxxxxx> >> Signed-off-by: Dan Williams <dan.j.williams@xxxxxxxxx> > > Reviewed-by: Vlastimil Babka <vbabka@xxxxxxx> > > vbabka@gusiac:~/wrk/cbmc> cbmc test-thp.c > CBMC version 5.3 64-bit x86_64 linux > Parsing test-thp.c > file <command-line> line 0: <command-line>:0:0: warning: > "__STDC_VERSION__" redefined > file <command-line> line 0: <built-in>: note: this is the location of > the previous definition > Converting > Type-checking test-thp > file test-thp.c line 75 function main: function `assert' is not declared > Generating GOTO Program > Adding CPROVER library > Function Pointer Removal > Partial Inlining > Generic Property Instrumentation > Starting Bounded Model Checking > size of program expression: 171 steps > simple slicing removed 3 assignments > Generated 1 VCC(s), 1 remaining after simplification > Passing problem to propositional reduction > converting SSA > Running propositional reduction > Post-processing > Solving with MiniSAT 2.2.0 with simplifier > 4899 variables, 13228 clauses > SAT checker: negated claim is UNSATISFIABLE, i.e., holds > Runtime decision procedure: 0.008s > VERIFICATION SUCCESSFUL > > (and yeah, the v1 version fails :) Can you share the test-thp.c so I can add this to my test collection? I'm assuming cbmc is "Bounded Model Checker for C/C++"?
