Skip to content

Commit afccaec

Browse files
committed
Provide goto-cc in performance tests
1 parent f802d87 commit afccaec

File tree

2 files changed

+13
-4
lines changed

2 files changed

+13
-4
lines changed

scripts/perf-test/codebuild.yaml

+2
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,7 @@ Resources:
7979
artifacts:
8080
files:
8181
- src/cbmc/cbmc
82+
- src/goto-cc/goto-cc
8283
- COMMIT_INFO
8384
discard-paths: yes
8485
Type: !Ref RepoType
@@ -121,6 +122,7 @@ Resources:
121122
artifacts:
122123
files:
123124
- src/cbmc/cbmc
125+
- src/goto-cc/goto-cc
124126
- COMMIT_INFO
125127
discard-paths: yes
126128
Type: !Ref RepoType

scripts/perf-test/ec2.yaml

+11-4
Original file line numberDiff line numberDiff line change
@@ -212,7 +212,7 @@ Resources:
212212
cd /mnt
213213
cd cprover-sv-comp
214214
git pull
215-
mkdir -p src/cbmc/
215+
mkdir -p src/cbmc src/goto-cc
216216
touch LICENSE
217217
cd ..
218218
mkdir -p run
@@ -292,10 +292,12 @@ Resources:
292292
--receipt-handle $msg
293293

294294
cd /mnt/cprover-sv-comp
295-
rm -f src/cbmc/cbmc
295+
rm -f src/cbmc/cbmc src/goto-cc/goto-cc
296296
aws s3 cp s3://${S3Bucket}/${PerfTestId}/$cfg/cbmc \
297297
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
299301
make CBMC=. cbmc.zip
300302
cd ../run
301303
unzip ../cprover-sv-comp/cbmc.zip
@@ -357,11 +359,16 @@ Resources:
357359
-N $max_par -c 1
358360
if ls *.gmon.out.* >/dev/null 2>&1
359361
then
360-
gprof --sum ./cbmc-binary *.gmon.out.*
362+
gprof --sum ./cbmc-binary cbmc*.gmon.out.*
361363
gprof ./cbmc-binary gmon.sum > sum.profile-$t
364+
rm -f gmon.sum
365+
gprof --sum ./goto-cc goto-cc*.gmon.out.*
366+
gprof ./goto-cc gmon.sum > sum.goto-cc-profile-$t
362367
rm -f gmon.sum gmon.out *.gmon.out.*
363368
aws s3 cp sum.profile-$t \
364369
s3://${S3Bucket}/${PerfTestId}/$cfg/sum.profile-$t
370+
aws s3 cp sum.goto-cc-profile-$t \
371+
s3://${S3Bucket}/${PerfTestId}/$cfg/sum.goto-cc-profile-$t
365372
fi
366373
fi
367374
rm -rf logs-$t sum.profile-$t

0 commit comments

Comments
 (0)