From 7071b89cc53654a9d8d5803a40f09b3c36b0967c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 10 May 2022 19:56:11 +0000 Subject: [PATCH 1/2] Test: unconstrained pointer need not be dynamic object Depending on the model returned by the solver, the unconstrained pointer could fail one of several assertions: it need not be a dynamic object, and the test specification should accept that. --- regression/cbmc-library/free-01/test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/cbmc-library/free-01/test.desc b/regression/cbmc-library/free-01/test.desc index 769ba573e7c..a727d0817d0 100644 --- a/regression/cbmc-library/free-01/test.desc +++ b/regression/cbmc-library/free-01/test.desc @@ -1,7 +1,7 @@ CORE main.c --pointer-check --bounds-check --stop-on-fail -free argument must be NULL or valid pointer +free argument must be (NULL or valid pointer|dynamic object) ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ From ae439ed020738cf8a65b859d5cbe635130d98996 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 10 May 2022 20:07:37 +0000 Subject: [PATCH 2/2] JBMC tests: constrain length of non-deterministic input string A solver may return a model that results in generating a string that would exceed available memory. --- .../jbmc-strings/ConstantEvaluationContains/nondetArg.desc | 2 +- .../jbmc-strings/ConstantEvaluationContains/noprop.desc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc index b4db9cfcef3..a7f4773db73 100644 --- a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc @@ -1,6 +1,6 @@ CORE Main ---function Main.nondetArg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +--function Main.nondetArg --max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` ^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc index bdddbfaed8f..068164f2d7b 100644 --- a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc @@ -1,6 +1,6 @@ CORE Main ---function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +--function Main.noprop --max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` ^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ ^EXIT=10$ ^SIGNAL=0$