@@ -803,6 +803,9 @@ abstract class AbstractCompiler
803803 self .header .add_decl ("extern int glob_argc; " )
804804 self .header .add_decl ("extern char **glob_argv; " )
805805 self .header .add_decl ("extern val *glob_sys; " )
806+
807+ # Global fonction used by the contract infrastructure
808+ self .header .add_decl ("extern int *getInAssertion(); // Used to know if we are currently checking some assertions. " )
806809 end
807810
808811 # Stack stocking environment for longjumps
@@ -942,6 +945,28 @@ extern void nitni_global_ref_decr( struct nitni_ref *ref );
942945 }
943946 return data;
944947 }
948+
949+ static pthread_key_t in_assertion_key;
950+ static pthread_once_t in_assertion_key_created = PTHREAD_ONCE_INIT;
951+
952+ static void create_in_assertion()
953+ {
954+ pthread_key_create(&in_assertion_key, NULL);
955+ }
956+
957+ //Flag used to know if we are currently checking some assertions.
958+ int *getInAssertion()
959+ {
960+ pthread_once(&in_assertion_key_created, &create_in_assertion);
961+ int* in_assertion = pthread_getspecific(in_assertion_key);
962+ if (in_assertion == NULL) {
963+ in_assertion = malloc(sizeof(int));
964+ *in_assertion = 0;
965+ pthread_setspecific(in_assertion_key, in_assertion);
966+ }
967+ return in_assertion;
968+ }
969+
945970#else
946971 // Use __thread when available
947972 __thread struct catch_stack_t catchStack = {-1, 0, NULL};
@@ -950,6 +975,12 @@ extern void nitni_global_ref_decr( struct nitni_ref *ref );
950975 {
951976 return &catchStack;
952977 }
978+
979+ __thread int in_assertion = 0; // Flag used to know if we are currently checking some assertions.
980+
981+ int *getInAssertion(){
982+ return &in_assertion;
983+ }
953984#endif
954985"""
955986
@@ -3858,6 +3889,18 @@ redef class AIfExpr
38583889 end
38593890end
38603891
3892+ redef class AIfInAssertion
3893+
3894+ redef fun stmt (v )
3895+ do
3896+ v .add ("if (~*getInAssertion())\{ " )
3897+ v .add ("*getInAssertion() = 1; " )
3898+ v .stmt (self .n_body )
3899+ v .add ("*getInAssertion() = 0; " )
3900+ v .add ("\} " )
3901+ end
3902+ end
3903+
38613904redef class AIfexprExpr
38623905 redef fun expr (v )
38633906 do
0 commit comments