Skip to content

Commit 4a8d69f

Browse files
Update path for cbmc output
1 parent 11de874 commit 4a8d69f

File tree

3 files changed

+8
-3
lines changed

3 files changed

+8
-3
lines changed

.gitignore

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,4 +10,7 @@ build/
1010
# Ignore code coverage artifacts
1111
*.gcda
1212
*.gcno
13-
*.gcov
13+
*.gcov
14+
15+
#Ignore cbmc output
16+
run.json

test/cbmc/run_proofs.sh

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
coreJSONDir="coreJSON"
44
tinyCborDir="tinycbor"
55
MQTTStreamingSourceDir="../../source"
6+
outputDir = "output/latest/html"
67

78
UNWIND_COUNT=${UNWIND_COUNT:-10}
89

@@ -11,14 +12,15 @@ if [ ! -d "$coreJSONDir" ]; then
1112
git clone https://github.com/FreeRTOS/coreJSON.git --depth 1 --branch v3.2.0
1213
fi
1314

15+
1416
exec cbmc stubs/strnlen.c stubs/JSON_SearchT.c stubs/tinycbor.c proofs.c \
1517
$MQTTStreamingSourceDir/MQTTFileDownloader.c \
1618
$MQTTStreamingSourceDir/MQTTFileDownloader_cbor.c \
1719
$MQTTStreamingSourceDir/MQTTFileDownloader_base64.c \
1820
-I $MQTTStreamingSourceDir/include -I coreJSON/source/include -I include \
1921
--unwindset strlen.0:36 \
20-
--strncat.0:192 \
21-
--strncat.1:205 \
22+
--unwindset strncat.0:192 \
23+
--unwindset strncat.1:205 \
2224
--bounds-check --pointer-check --memory-cleanup-check --div-by-zero-check \
2325
--signed-overflow-check --unsigned-overflow-check --pointer-overflow-check \
2426
--conversion-check --undefined-shift-check --enum-range-check \

0 commit comments

Comments
 (0)