File tree Expand file tree Collapse file tree 2 files changed +12
-4
lines changed Expand file tree Collapse file tree 2 files changed +12
-4
lines changed Original file line number Diff line number Diff line change @@ -80,6 +80,7 @@ Resources:
80
80
artifacts:
81
81
files:
82
82
- src/cbmc/cbmc
83
+ - src/goto-cc/goto-cc
83
84
- COMMIT_INFO
84
85
discard-paths: yes
85
86
Type : !Ref RepoType
@@ -123,6 +124,7 @@ Resources:
123
124
artifacts:
124
125
files:
125
126
- src/cbmc/cbmc
127
+ - src/goto-cc/goto-cc
126
128
- COMMIT_INFO
127
129
discard-paths: yes
128
130
Type : !Ref RepoType
Original file line number Diff line number Diff line change @@ -212,7 +212,7 @@ Resources:
212
212
cd /mnt
213
213
cd cprover-sv-comp
214
214
git pull
215
- mkdir -p src/cbmc/
215
+ mkdir -p src/cbmc src/goto-cc
216
216
touch LICENSE
217
217
cd ..
218
218
mkdir -p run
@@ -292,10 +292,12 @@ Resources:
292
292
--receipt-handle $msg
293
293
294
294
cd /mnt/cprover-sv-comp
295
- rm -f src/cbmc/cbmc
295
+ rm -f src/cbmc/cbmc src/goto-cc/goto-cc
296
296
aws s3 cp s3://${S3Bucket}/${PerfTestId}/$cfg/cbmc \
297
297
src/cbmc/cbmc
298
- chmod a+x src/cbmc/cbmc
298
+ aws s3 cp s3://${S3Bucket}/${PerfTestId}/$cfg/goto-cc \
299
+ src/goto-cc/goto-cc
300
+ chmod a+x src/cbmc/cbmc src/goto-cc/goto-cc
299
301
make CBMC=. cbmc.zip
300
302
cd ../run
301
303
unzip ../cprover-sv-comp/cbmc.zip
@@ -357,11 +359,15 @@ Resources:
357
359
-N $max_par -c 1
358
360
if ls *.gmon.out.* >/dev/null 2>&1
359
361
then
360
- gprof --sum ./cbmc-binary *.gmon.out.*
362
+ gprof --sum ./cbmc-binary cbmc *.gmon.out.*
361
363
gprof ./cbmc-binary gmon.sum > sum.profile-$t
364
+ gprof --sum ./goto-cc goto-cc*.gmon.out.*
365
+ gprof ./goto-cc gmon.sum > sum.goto-cc-profile-$t
362
366
rm -f gmon.sum gmon.out *.gmon.out.*
363
367
aws s3 cp sum.profile-$t \
364
368
s3://${S3Bucket}/${PerfTestId}/$cfg/sum.profile-$t
369
+ aws s3 cp sum.goto-cc-profile-$t \
370
+ s3://${S3Bucket}/${PerfTestId}/$cfg/sum.profile-$t
365
371
fi
366
372
fi
367
373
rm -rf logs-$t sum.profile-$t
You can’t perform that action at this time.
0 commit comments