Skip to content
Snippets Groups Projects
Commit 2dbffd79 authored by Fonenantsoa Maurica's avatar Fonenantsoa Maurica
Browse files

Subtraction between pointers gives integer.

parent 84290a11
No related branches found
No related tags found
No related merge requests found
...@@ -19,6 +19,8 @@ ...@@ -19,6 +19,8 @@
# configure configure # configure configure
############################################################################### ###############################################################################
-* E-ACSL [2018/10/04] Fix bug #2386 about incorrect typing when
performing pointer subtraction.
-* E-ACSL [2018/10/04] Support for \at on purely logic variables. -* E-ACSL [2018/10/04] Support for \at on purely logic variables.
Fix bug #1762 about out-of-scope variables when using \old. Fix bug #1762 about out-of-scope variables when using \old.
* E-ACSL [2018/10/02] Fix bug #2305 about taking the address of a * E-ACSL [2018/10/02] Fix bug #2305 about taking the address of a
......
/* run.config, run.config_2
COMMENT: pointer substraction
COMMENT: on gcc_x86_64
LOG: gen_@PTEST_NAME@.c
OPT: -machdep gcc_x86_64 -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -value-verbose 0
COMMENT: on x86_32 (default case when no machdep is given)
LOG: gen_@PTEST_NAME@_2.c
OPT: -machdep x86_32 -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@_2.c -kernel-verbose 0 -val -value-verbose 0
COMMENT: with "-e-acsl-gmp-only"
LOG: gen_@PTEST_NAME@_3.c
OPT: -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@_3.c -kernel-verbose 0 -val -value-verbose 0
*/
void f(const void *s, int c, unsigned long n) {
const unsigned char *p = s;
/*@ assert p - s == n - n; */
/*@ assert p - s == 0; */
}
int main() {
const char *s = "1234567890";
f(s, '0', 11);
return 0;
}
\ No newline at end of file
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/bts/bts2386.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/bts/bts2386.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/bts/bts2386.c:17: Warning:
function __e_acsl_assert: precondition got status unknown.
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string;
void f(void const *s, int c, unsigned long n)
{
__e_acsl_store_block((void *)(& s),(size_t)8);
unsigned char const *p = (unsigned char const *)s;
__e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
/*@ assert p - (unsigned char const *)s ≡ n - n; */
{
__e_acsl_mpz_t __gen_e_acsl_;
__e_acsl_mpz_t __gen_e_acsl_n;
__e_acsl_mpz_t __gen_e_acsl_sub;
int __gen_e_acsl_eq;
__gmpz_init_set_ui(__gen_e_acsl_,p - (unsigned char const *)s);
__gmpz_init_set_ui(__gen_e_acsl_n,n);
__gmpz_init(__gen_e_acsl_sub);
__gmpz_sub(__gen_e_acsl_sub,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
__gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sub));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"f",
(char *)"p - (unsigned char const *)s == n - n",16);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl_n);
__gmpz_clear(__gen_e_acsl_sub);
}
/*@ assert p - (unsigned char const *)s ≡ 0; */
__e_acsl_assert(p - (unsigned char const *)s == 0UL,(char *)"Assertion",
(char *)"f",(char *)"p - (unsigned char const *)s == 0",17);
__e_acsl_delete_block((void *)(& s));
__e_acsl_delete_block((void *)(& p));
return;
}
void __e_acsl_globals_init(void)
{
__gen_e_acsl_literal_string = "1234567890";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,
sizeof("1234567890"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
return;
}
int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
char const *s = __gen_e_acsl_literal_string;
__e_acsl_store_block((void *)(& s),(size_t)8);
__e_acsl_full_init((void *)(& s));
f((void const *)s,'0',(unsigned long)11);
__retres = 0;
__e_acsl_delete_block((void *)(& s));
__e_acsl_memory_clean();
return __retres;
}
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string;
void f(void const *s, int c, unsigned long n)
{
__e_acsl_store_block((void *)(& s),(size_t)4);
unsigned char const *p = (unsigned char const *)s;
__e_acsl_store_block((void *)(& p),(size_t)4);
__e_acsl_full_init((void *)(& p));
/*@ assert p - (unsigned char const *)s ≡ n - n; */
__e_acsl_assert(p - (unsigned char const *)s == n - (long long)n,
(char *)"Assertion",(char *)"f",
(char *)"p - (unsigned char const *)s == n - n",16);
/*@ assert p - (unsigned char const *)s ≡ 0; */
__e_acsl_assert(p - (unsigned char const *)s == 0U,(char *)"Assertion",
(char *)"f",(char *)"p - (unsigned char const *)s == 0",17);
__e_acsl_delete_block((void *)(& s));
__e_acsl_delete_block((void *)(& p));
return;
}
void __e_acsl_globals_init(void)
{
__gen_e_acsl_literal_string = "1234567890";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,
sizeof("1234567890"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
return;
}
int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)4);
__e_acsl_globals_init();
char const *s = __gen_e_acsl_literal_string;
__e_acsl_store_block((void *)(& s),(size_t)4);
__e_acsl_full_init((void *)(& s));
f((void const *)s,'0',(unsigned long)11);
__retres = 0;
__e_acsl_delete_block((void *)(& s));
__e_acsl_memory_clean();
return __retres;
}
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string;
void f(void const *s, int c, unsigned long n)
{
__e_acsl_store_block((void *)(& s),(size_t)4);
unsigned char const *p = (unsigned char const *)s;
__e_acsl_store_block((void *)(& p),(size_t)4);
__e_acsl_full_init((void *)(& p));
/*@ assert p - (unsigned char const *)s ≡ n - n; */
{
__e_acsl_mpz_t __gen_e_acsl_;
__e_acsl_mpz_t __gen_e_acsl_n;
__e_acsl_mpz_t __gen_e_acsl_sub;
int __gen_e_acsl_eq;
__gmpz_init_set_ui(__gen_e_acsl_,
(unsigned long)(p - (unsigned char const *)s));
__gmpz_init_set_ui(__gen_e_acsl_n,n);
__gmpz_init(__gen_e_acsl_sub);
__gmpz_sub(__gen_e_acsl_sub,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
__gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sub));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"f",
(char *)"p - (unsigned char const *)s == n - n",16);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl_n);
__gmpz_clear(__gen_e_acsl_sub);
}
/*@ assert p - (unsigned char const *)s ≡ 0; */
{
__e_acsl_mpz_t __gen_e_acsl__2;
__e_acsl_mpz_t __gen_e_acsl__3;
int __gen_e_acsl_eq_2;
__gmpz_init_set_ui(__gen_e_acsl__2,
(unsigned long)(p - (unsigned char const *)s));
__gmpz_init_set_si(__gen_e_acsl__3,0L);
__gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"f",
(char *)"p - (unsigned char const *)s == 0",17);
__gmpz_clear(__gen_e_acsl__2);
__gmpz_clear(__gen_e_acsl__3);
}
__e_acsl_delete_block((void *)(& s));
__e_acsl_delete_block((void *)(& p));
return;
}
void __e_acsl_globals_init(void)
{
__gen_e_acsl_literal_string = "1234567890";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,
sizeof("1234567890"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
return;
}
int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)4);
__e_acsl_globals_init();
char const *s = __gen_e_acsl_literal_string;
__e_acsl_store_block((void *)(& s),(size_t)4);
__e_acsl_full_init((void *)(& s));
f((void const *)s,'0',(unsigned long)11);
__retres = 0;
__e_acsl_delete_block((void *)(& s));
__e_acsl_memory_clean();
return __retres;
}
...@@ -483,7 +483,7 @@ and context_insensitive_term_to_exp kf env t = ...@@ -483,7 +483,7 @@ and context_insensitive_term_to_exp kf env t =
| TBinOp((BOr | BXor | BAnd), _, _) -> | TBinOp((BOr | BXor | BAnd), _, _) ->
(* other logic/arith operators *) (* other logic/arith operators *)
not_yet env "missing binary bitwise operator" not_yet env "missing binary bitwise operator"
| TBinOp(PlusPI | IndexPI | MinusPI | MinusPP as bop, t1, t2) -> | TBinOp(PlusPI | IndexPI | MinusPI as bop, t1, t2) ->
if Misc.is_set_of_ptr_or_array t1.term_type || if Misc.is_set_of_ptr_or_array t1.term_type ||
Misc.is_set_of_ptr_or_array t2.term_type then Misc.is_set_of_ptr_or_array t2.term_type then
(* case of arithmetic over set of pointers (due to use of ranges) (* case of arithmetic over set of pointers (due to use of ranges)
...@@ -497,6 +497,18 @@ and context_insensitive_term_to_exp kf env t = ...@@ -497,6 +497,18 @@ and context_insensitive_term_to_exp kf env t =
let e1, env = term_to_exp kf env t1 in let e1, env = term_to_exp kf env t1 in
let e2, env = term_to_exp kf env t2 in let e2, env = term_to_exp kf env t2 in
Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, false, "" Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, false, ""
| TBinOp(MinusPP, t1, t2) ->
begin match Typing.get_integer_ty t with
| Typing.C_type _ ->
let e1, env = term_to_exp kf env t1 in
let e2, env = term_to_exp kf env t2 in
let ty = Typing.get_typ t in
Cil.new_exp ~loc (BinOp(MinusPP, e1, e2, ty)), env, false, ""
| Typing.Gmp ->
not_yet env "pointer subtraction resulting in gmp"
| Typing.Other ->
assert false
end
| TCastE(ty, t') -> | TCastE(ty, t') ->
let e, env = term_to_exp kf env t' in let e, env = term_to_exp kf env t' in
let e, env = add_cast ~loc ~name:"cast" env (Some ty) false (Some t) e in let e, env = add_cast ~loc ~name:"cast" env (Some ty) false (Some t) e in
......
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