changeset | 44cc739b8b56 |
---|---|
branch | default |
bookmark | |
tag | tip |
user | atton |
description | Fix assert condition |
files | src/insert_verification/verifySpecification.c |
changeset | 517d1108f91f |
---|---|
branch | |
bookmark | |
tag | |
user | atton |
description | Tree height verification using cbmc |
files | cbmc/insert_verification/cbmcLLRBContext.c cbmc/insert_verification/include/cbmcLLRBContext.h cbmc/insert_verification/insert_verification.sh cbmc/insert_verification/main.c |
changeset | 3e6cd523bf6d |
---|---|
branch | |
bookmark | |
tag | |
user | atton |
description | Delete C function converted CS |
files | src/insert_verification/verifySpecification.c |
changeset | 23b9717a5c14 |
---|---|
branch | |
bookmark | |
tag | |
user | atton |
description | Fix include |
files | src/insert_verification/verifySpecification.c |
changeset | 9240d7ca8b5d |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Merge |
files |
changeset | 6bf95d172d46 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Update Dockerfile |
files | cbmc/Dockerfile |
changeset | 56ea709e7af3 |
---|---|
branch | |
bookmark | |
tag | |
user | atton |
description | Fix SEGV |
files | src/insert_verification/akashaLLRBContext.c src/insert_verification/include/akashaLLRBContext.h src/insert_verification/main.c src/insert_verification/verifySpecification.c |
changeset | 81717f43ea00 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Convert C function to cs (getMaxHeight) |
files | src/insert_verification/include/akashaLLRBContext.h src/insert_verification/verifySpecification.c |
changeset | 593ab851ad76 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Convert C function to cs (getMinHeight) |
files | src/insert_verification/akashaLLRBContext.c src/insert_verification/include/akashaLLRBContext.h src/insert_verification/main.c src/insert_verification/verifySpecification.c |
changeset | e27f4961281e |
---|---|
branch | |
bookmark | |
tag | |
user | atton |
description | WIP: insert verification using cbmc (syntax valid) |
files | cbmc/insert_verification/cbmcCS.c cbmc/insert_verification/cbmcLLRBContext.c cbmc/insert_verification/include/cbmcCS.h cbmc/insert_verification/include/cbmcLLRBContext.h cbmc/insert_verification/include/llrbContext.h cbmc/insert_verification/include/origin_cs.h cbmc/insert_verification/insert_verification.sh cbmc/insert_verification/main.c |