Skip to content
Snippets Groups Projects
Commit 610f7297 authored by Andre Maroneze's avatar Andre Maroneze Committed by Virgile Prevosto
Browse files

[tests] remove excessively large libc oracles to avoid conflicts

parent b3b4062f
No related branches found
No related tags found
No related merge requests found
...@@ -3,7 +3,7 @@ NOFRAMAC: use execnow for proper sequencing of executions ...@@ -3,7 +3,7 @@ NOFRAMAC: use execnow for proper sequencing of executions
EXECNOW: BIN @PTEST_NAME@_parse.sav LOG @PTEST_NAME@.parse.log LOG @PTEST_NAME@.parse.err @frama-c@ @PTEST_FILE@ -save ./@PTEST_NAME@_parse.sav > ./@PTEST_NAME@.parse.log 2> ./@PTEST_NAME@.parse.err EXECNOW: BIN @PTEST_NAME@_parse.sav LOG @PTEST_NAME@.parse.log LOG @PTEST_NAME@.parse.err @frama-c@ @PTEST_FILE@ -save ./@PTEST_NAME@_parse.sav > ./@PTEST_NAME@.parse.log 2> ./@PTEST_NAME@.parse.err
EXECNOW: BIN @PTEST_NAME@_eva.sav LOG @PTEST_NAME@.eva.log LOG @PTEST_NAME@.eva.err @frama-c@ -load %{dep:./@PTEST_NAME@_parse.sav} -eva -save ./@PTEST_NAME@_eva.sav > ./@PTEST_NAME@.eva.log 2> ./@PTEST_NAME@.eva.err EXECNOW: BIN @PTEST_NAME@_eva.sav LOG @PTEST_NAME@.eva.log LOG @PTEST_NAME@.eva.err @frama-c@ -load %{dep:./@PTEST_NAME@_parse.sav} -eva -save ./@PTEST_NAME@_eva.sav > ./@PTEST_NAME@.eva.log 2> ./@PTEST_NAME@.eva.err
EXECNOW: BIN @PTEST_NAME@.sarif.unfiltered LOG @PTEST_NAME@.sarif.log LOG @PTEST_NAME@.sarif.err @frama-c@ -load %{dep:./@PTEST_NAME@_eva.sav} -then -mdr-out ./@PTEST_NAME@.sarif.unfiltered -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic > ./@PTEST_NAME@.sarif.log 2> ./@PTEST_NAME@.sarif.err EXECNOW: BIN @PTEST_NAME@.sarif.unfiltered LOG @PTEST_NAME@.sarif.log LOG @PTEST_NAME@.sarif.err @frama-c@ -load %{dep:./@PTEST_NAME@_eva.sav} -then -mdr-out ./@PTEST_NAME@.sarif.unfiltered -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic > ./@PTEST_NAME@.sarif.log 2> ./@PTEST_NAME@.sarif.err
EXECNOW: LOG @PTEST_NAME@.sarif sed -e "s:@PTEST_SESSION@:PTEST_SESSION:" %{dep:@PTEST_NAME@.sarif.unfiltered} > @PTEST_NAME@.sarif 2> @NULL EXECNOW: LOG @PTEST_NAME@.sarif sed -e "s:@PTEST_SESSION@:PTEST_SESSION:" %{dep:@PTEST_NAME@.sarif.unfiltered} > @PTEST_NAME@.sarif 2> @DEV_NULL@
*/ */
#include "__fc_builtin.h" #include "__fc_builtin.h"
#define LENGTH 10 #define LENGTH 10
......
/* run.config /* run.config
CMD: @frama-c@ -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic CMD: @frama-c@ -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic
BIN: with-libc.sarif.unfiltered BIN: with-libc.sarif.unchecked
OPT: -mdr-out ./with-libc.sarif.unfiltered OPT: -mdr-out ./with-libc.sarif.unchecked
EXECNOW: LOG with-libc.sarif sed -e "s:@PTEST_SESSION@:PTEST_SESSION:" %{dep:with-libc.sarif.unfiltered} > with-libc.sarif 2> @NULL COMMENT: the log with libc is too large, so we do not use it as textual oracle
BIN: without-libc.sarif.unfiltered BIN: without-libc.sarif.unfiltered
OPT: -mdr-no-print-libc -mdr-out ./without-libc.sarif.unfiltered OPT: -mdr-no-print-libc -mdr-out ./without-libc.sarif.unfiltered
EXECNOW: LOG without-libc.sarif sed -e "s:@PTEST_SESSION@:PTEST_SESSION:" %{dep:without-libc.sarif.unfiltered} > without-libc.sarif 2> @NULL EXECNOW: LOG without-libc.sarif sed -e "s:@PTEST_SESSION@:PTEST_SESSION:" %{dep:without-libc.sarif.unfiltered} > without-libc.sarif 2> @DEV_NULL@
*/ */
#include <string.h> #include <string.h>
int main() { int main() {
......
...@@ -17,4 +17,4 @@ ...@@ -17,4 +17,4 @@
Preconditions 1 valid 0 unknown 0 invalid 1 total Preconditions 1 valid 0 unknown 0 invalid 1 total
100% of the logical properties reached have been proven. 100% of the logical properties reached have been proven.
---------------------------------------------------------------------------- ----------------------------------------------------------------------------
[mdr] Report with-libc.sarif.unfiltered generated [mdr] Report with-libc.sarif.unchecked generated
[kernel] Parsing std_string.c (with preprocessing) [kernel] Parsing std_print.c (with preprocessing)
[eva] Analyzing a complete application starting at main [eva] Analyzing a complete application starting at main
[eva:initial-state] Values of globals at initialization [eva:initial-state] Values of globals at initialization
...@@ -16,4 +16,4 @@ ...@@ -16,4 +16,4 @@
---------------------------------------------------------------------------- ----------------------------------------------------------------------------
No logical properties have been reached by the analysis. No logical properties have been reached by the analysis.
---------------------------------------------------------------------------- ----------------------------------------------------------------------------
[mdr] Report std_string.sarif.unfiltered generated [mdr] Report std_print.sarif.unfiltered generated
{
"$schema": "https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json",
"version": "2.1.0",
"runs": [
{
"tool": {
"driver": {
"name": "frama-c",
"fullName": "frama-c-0+omitted-for-deterministic-output",
"version": "0+omitted-for-deterministic-output",
"downloadUri": "https://frama-c.com/download.html",
"informationUri": "https://frama-c.com"
}
},
"invocations": [
{
"commandLine": "frama-c -check -no-autoload-plugins -add-symbolic-path=PTEST_SESSION:. -load-plugin=eva,from,scope,inout,markdown-report std_print.c -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out ./std_print.sarif.unfiltered",
"arguments": [
"-check", "-no-autoload-plugins",
"-add-symbolic-path=PTEST_SESSION:.",
"-load-plugin=eva,from,scope,inout,markdown-report",
"std_print.c", "-eva", "-then", "-mdr-sarif-deterministic",
"-mdr-gen", "sarif", "-mdr-out", "./std_print.sarif.unfiltered"
],
"exitCode": 0,
"executionSuccessful": true
}
],
"originalUriBaseIds": {
".": { "uri": "file:///omitted-for-deterministic-output/" },
"PWD": { "uri": "file:///omitted-for-deterministic-output/" }
},
"artifacts": [
{
"location": { "uri": "std_print.c", "uriBaseId": "PWD" },
"roles": [ "analysisTarget" ],
"mimeType": "text/x-csrc"
}
],
"defaultSourceLanguage": "C",
"taxonomies": [
{ "name": "frama-c", "contents": [ "nonLocalizedData" ] }
]
}
]
}
This diff is collapsed.
This diff is collapsed.
/* run.config* /* run.config*
BIN: @PTEST_NAME@.sarif.unfiltered BIN: @PTEST_NAME@.sarif.unfiltered
OPT: -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out ./@PTEST_NAME@.sarif.unfiltered OPT: -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out ./@PTEST_NAME@.sarif.unfiltered
EXECNOW: LOG @PTEST_NAME@.sarif sed -e "s:@PTEST_SESSION@:PTEST_SESSION:" %{dep:@PTEST_NAME@.sarif.unfiltered} > @PTEST_NAME@.sarif 2> @NULL EXECNOW: LOG @PTEST_NAME@.sarif sed -e "s:@PTEST_SESSION@:PTEST_SESSION:" %{dep:@PTEST_NAME@.sarif.unfiltered} > @PTEST_NAME@.sarif 2> @DEV_NULL@
COMMENT: tests printing a SARIF file with a source from the libc; we choose a small one to avoid a huge SARIF oracle
*/ */
#include "string.c" #include "errno.c"
int main() { } int main() { }
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
MODULE: check_libc_naming_conventions, check_const MODULE: check_libc_naming_conventions, check_const
OPT: -load %{dep:@PTEST_NAME@.sav} -print -cpp-extra-args='-nostdinc -I@FRAMAC_SHARE@/libc' -eva @EVA_CONFIG@ -then -lib-entry -no-print OPT: -load %{dep:@PTEST_NAME@.sav} -print -cpp-extra-args='-nostdinc -I@FRAMAC_SHARE@/libc' -eva @EVA_CONFIG@ -then -lib-entry -no-print
MODULE: MODULE:
OPT: -print -print-libc -machdep x86_32 OPT: -print -print-libc -machdep x86_32 -ocode @DEV_NULL@
MODULE: check_parsing_individual_headers MODULE: check_parsing_individual_headers
OPT: OPT:
MODULE: check_libc_anonymous_tags MODULE: check_libc_anonymous_tags
......
This diff is collapsed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment