source: CIVL/examples/loop_invariants/loop_assigns_gen

main
Name Size Rev Age Author Last Change
../
twoLoops.cvl 238 bytes ​ ea777aa   – – –
twoLoops2.cvl 200 bytes ​ ea777aa   – – –
summation.cvl 316 bytes ​ ea777aa   – – –
summation-bad_invariant.cvl 349 bytes ​ ea777aa   – – –
summation-bad_assert.cvl 337 bytes ​ ea777aa   – – –
selectSort.cvl 857 bytes ​ ea777aa   – – –
selectSort-bad_think.cvl 1.1 KB ​ ea777aa   – – –
selectSort-bad_invariants.cvl 873 bytes ​ ea777aa   – – –
selectSort-bad_assert.cvl 873 bytes ​ ea777aa   – – –
relaxedPrefix_loop.cvl 1.8 KB ​ ea777aa   – – –
max.cvl 379 bytes ​ ea777aa   – – –
max-bad_invariants.cvl 413 bytes ​ ea777aa   – – –
max-bad_assert.cvl 414 bytes ​ ea777aa   – – –
max2.cvl 774 bytes ​ ea777aa   – – –
Makefile 200 bytes ​ ea777aa   – – –
lcp2.cvl 4.5 KB ​ ea777aa   – – –
binarySearch.cvl 575 bytes ​ ea777aa   – – –
arrayZeroes2d_column_preserve.cvl 442 bytes ​ ea777aa   – – –
arrayZeroes2d_column.cvl 402 bytes ​ ea777aa   – – –
arrayZeroes2d_column-bad_invariant.cvl 404 bytes ​ ea777aa   – – –
arrayZeroes2d_column-bad_assert.cvl 408 bytes ​ ea777aa   – – –
arrayZeroes2d_2columns_preserve.cvl 538 bytes ​ ea777aa   – – –
arrayZeroes2d_2columns_preserve-bad_assert.cvl 522 bytes ​ ea777aa   – – –
arrayZeroes2d_2columns.cvl 455 bytes ​ ea777aa   – – –
arrayZeroes2d.cvl 837 bytes ​ ea777aa   – – –
arrayZeroes2d-bad_invariants.cvl 693 bytes ​ ea777aa   – – –
arrayZeroes2d-bad_assert.cvl 693 bytes ​ ea777aa   – – –
arrayZeroes1d.cvl 417 bytes ​ ea777aa   – – –
arrayZeroes1d-bad.cvl 417 bytes ​ ea777aa   – – –
arrayEqualsNoReturn.cvl 513 bytes ​ ea777aa   – – –
arrayEqualsNoReturn-bad_impl.cvl 468 bytes ​ ea777aa   – – –
arrayEqualsNoReturn-bad_assert.cvl 513 bytes ​ ea777aa   – – –
arrayEquals_early_return.cvl 523 bytes ​ ea777aa   – – –
arrayEquals.cvl 545 bytes ​ ea777aa   – – –
arrayEquals-bug.cvl 539 bytes ​ ea777aa   – – –
arrayEquals2.cvl 522 bytes ​ ea777aa   – – –
  • Property mode set to 040000
Note: See TracBrowser for help on using the repository browser.