Skip to content
Snippets Groups Projects
Commit fbdb744c authored by Patrick Baudin's avatar Patrick Baudin
Browse files

use MODULE directive instead of CMXS

parent eb280784
No related branches found
No related tags found
No related merge requests found
Showing
with 41 additions and 41 deletions
/* run.config
CMXS: @PTEST_NAME@
OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print -constfold
MODULE: @PTEST_NAME@.cmxs
STDOPT: +"-constfold"
*/
int main(void) {
......
/* run.config
PLUGIN: report
CMXS: @PTEST_NAME@
OPT: -load-module %{dep:@PTEST_NAME@.cmxs} -then -report -then -print
MODULE: @PTEST_NAME@.cmxs
OPT: -then -report -then -print
*/
/*@ assigns *x; */
......
/* run.config
CMXS: @PTEST_NAME@
OPT: -typecheck -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}
MODULE: @PTEST_NAME@.cmxs
OPT: -typecheck
*/
/* must emit falls-through warning. */
int f (int foo, char** args) {
......
/* run.config
CMXS: @PTEST_NAME@
OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}
MODULE: @PTEST_NAME@.cmxs
OPT:
*/
typedef unsigned char uint8_t;
......
/* run.config
CMXS: @PTEST_NAME@
OPT: -eva-verbose 2 -load-module %{dep:@PTEST_NAME@.cmxs} -print
MODULE: @PTEST_NAME@.cmxs
OPT: -eva-verbose 2 -print
*/
void main() { //@ assert \true;
}
......
/* run.config
PLUGIN: report
CMXS: @PTEST_NAME@
OPT: @EVA_OPTIONS@ -load-module %{dep:@PTEST_NAME@.cmxs} -then -report
MODULE: @PTEST_NAME@.cmxs
OPT: @EVA_OPTIONS@ -then -report
*/
int f(int *x) { return *x; }
int g(int *x) { return *(x++); }
/* run.config
CMXS: @PTEST_NAME@
OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}
MODULE: @PTEST_NAME@.cmxs
OPT:
*/
// Don't use -debug 1 option in the test command.
......
/* run.config*
CMXS: @PTEST_NAME@
OPT: -eva -main f -load-module %{dep:@PTEST_NAME@.cmxs} -then-on change_main -main g -eva
MODULE: @PTEST_NAME@.cmxs
OPT: -eva -main f -then-on change_main -main g -eva
*/
int f(int x) { return x; }
/* run.config
CMXS: @PTEST_NAME@
OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -multiple-map a:1,b:2,a:3
MODULE: @PTEST_NAME@.cmxs
OPT: -multiple-map a:1,b:2,a:3
*/
/* run.config
CMXS: @PTEST_NAME@
OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}
MODULE: @PTEST_NAME@.cmxs
OPT:
*/
/*@ requires \valid(p); assigns *p; ensures *p == x; */
......
/* run.config
CMXS: @PTEST_NAME@
OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -machdep x86_64 -enums int -no-unicode
MODULE: @PTEST_NAME@.cmxs
OPT: -machdep x86_64 -enums int -no-unicode
*/
int main () { return 0; }
/* run.config
CMXS: @PTEST_NAME@
OPT: -load-module %{dep:@PTEST_NAME@.cmxs}
MODULE: @PTEST_NAME@.cmxs
OPT:
*/
//@ ensures *p==1;
void main(int * p){ *p = 0; }
/* run.config
CMXS: @PTEST_NAME@
OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print
OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -remove-exn -print
MODULE: @PTEST_NAME@.cmxs
OPT: -print
OPT: -remove-exn -print
*/
struct my_exn { int e; };
......
/* run.config
CMXS: global_decl_loc
OPT: %{dep:global_decl_loc2.i} -load-module %{dep:@PTEST_NAME@.cmxs}
MODULE: @PTEST_NAME@.cmxs
OPT: %{dep:global_decl_loc2.i}
*/
int g;
/* run.config
CMXS: @PTEST_NAME@
OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}
MODULE: @PTEST_NAME@.cmxs
OPT:
*/
int f(int x);
......
/* run.config
CMXS: @PTEST_NAME@
OPT: -eva @EVA_CONFIG@ -eva-slevel-function main:10 -load-module %{dep:@PTEST_NAME@.cmxs}
MODULE: @PTEST_NAME@.cmxs
OPT: -eva @EVA_CONFIG@ -eva-slevel-function main:10
*/
void main() {
int i, j = 0;
......
/* run.config
CMXS: @PTEST_NAME@
OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}
MODULE: @PTEST_NAME@.cmxs
OPT:
*/
/* run.config
CMXS: @PTEST_NAME@
OPT: -main f -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print
MODULE: @PTEST_NAME@.cmxs
OPT: -main f -print
*/
static int f(void);
......
/* run.config
CMXS: plugin_log
MODULE: plugin_log.cmxs
LOG: log-file-kernel-warnings.txt
LOG: log-file-kernel-results.txt
LOG: log-file-feedback.txt
......@@ -8,7 +8,7 @@
LOG: plugin-log-all.txt
FILTER: sed 's|Your Frama-C version is.*|Your Frama-C version is VERSION|'
STDOPT: #"-kernel-log w:@PTEST_RESULT@/log-file-kernel-warnings.txt,r:@PTEST_RESULT@/log-file-kernel-results.txt -eva-log f:@PTEST_RESULT@/log-file-feedback.txt,afewr:@PTEST_RESULT@/log-file-value-all.txt -eva-log :@PTEST_RESULT@/log-file-value-default.txt -then -kernel-log f:@PTEST_RESULT@/log-file-feedback.txt"
OPT: -load-module plugin_log -kernel-msg-key foo-category -kernel-log=a:@PTEST_RESULT@/plugin-log-all.txt
OPT: -kernel-msg-key foo-category -kernel-log=a:@PTEST_RESULT@/plugin-log-all.txt
DONTRUN: test disabled due to non-deterministic errors in CI
*/
int f(void); // generates kernel warning (missing spec)
......
/* run.config
CMXS: @PTEST_NAME@
OPT: @EVA_CONFIG@ -load-module %{dep:@PTEST_NAME@.cmxs}
MODULE: @PTEST_NAME@.cmxs
OPT: @EVA_CONFIG@
*/
int* f() {
......
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