Added Linked_list_tests

[emmyni]

• linked_list_front
• linked_list_begin
• linked_list_end
• linked_list_pop_front
• inked_list_init
• linked_list_reset
• linked_list_next

[agurfinkel]

If I am not mistaken these are based directly on cbmc style pfs.

While this is good as exercise, it is not the direction we decided to go with the pfs.

Maybe we can move them into some other directory to keep for comparison sake.

What are verification times for these?

[emmyni]

What is the difference between cbmc style and pfs and the other pfs?
For moving to a different directory, is there already a specific directory or should I make one?

Also is the verification time in the brunch stats?
************** BRUNCH STATS *****************
BRUNCH_STAT Result TRUE
BRUNCH_STAT bmc.circ_sz 72
BRUNCH_STAT bmc.dag_sz 398
BRUNCH_STAT BMC 0.02
BRUNCH_STAT BMC.solve 0.01
BRUNCH_STAT opsem.assert 0.00
BRUNCH_STAT opsem.simplify 0.00
BRUNCH_STAT seahorn_total 0.02
************** BRUNCH STATS END *****************

[danblitzhou]

What is the difference between cbmc style and pfs and the other pfs?
For moving to a different directory, is there already a specific directory or should I make one?

Also is the verification time in the brunch stats?
************** BRUNCH STATS *****************
BRUNCH_STAT Result TRUE
BRUNCH_STAT bmc.circ_sz 72
BRUNCH_STAT bmc.dag_sz 398
BRUNCH_STAT BMC 0.02
BRUNCH_STAT BMC.solve 0.01
BRUNCH_STAT opsem.assert 0.00
BRUNCH_STAT opsem.simplify 0.00
BRUNCH_STAT seahorn_total 0.02
************** BRUNCH STATS END *****************

1. From my understanding, CBMC style proofs create concrete linked list data structure of limited length and use bounded loop unrolling to reason correctness of functions on the linked list; the direction of proofs we are heading is more towards unbounded model checking if possbile, see refactor(jobs): common initialization code is refactored into helper … #20 by Siddarth for our modeling of linked list;
2. Create a directory in verify-c-common/seahorn; this is for separating test/experiment cases from main jobs
3. A quick way to see verification time is ctest -j32 -R linked_list, this should run all linked_list jobs and show you result and time