**François Bobot**
(df489f94)
*
at
23 Jan 03:37
*

Merge branch 'feature/andre/extlib-migrate-408' into 'master'

*
... and
9 more commits
*

**François Bobot**
(795e29e8)
*
at
22 Jan 03:50
*

Merge branch 'fix/andre/fc-script-make-4.1' into 'master'

*
... and
36 more commits
*

**François Bobot**
(6938fe66)
*
at
21 Jan 04:04
*

Merge branch 'fix/wp/opaque-struct' into 'master'

*
... and
6 more commits
*

**François Bobot**
(91fdc9e2)
*
at
20 Jan 04:09
*

Merge branch 'fix/aorai/yaparser-rule' into 'master'

*
... and
8 more commits
*

**François Bobot**
(45697b01)
*
at
19 Jan 03:34
*

Merge branch 'feature/basile/pretty-funbehavior' into 'master'

*
... and
6 more commits
*

- Frama-C installation mode:
*Opam* - Frama-C version:
*22.0 (Titanium)* - Plug-in used:
*WP* - OS name:
*Ubuntu* - OS version:
*Ubuntun 20.04.1 LTS*

*Please add specific information deemed relevant with regard to this issue.*

- Get the following C file (issue_shift.c):

```
#include <limits.h>
/*@
requires 0 <= a <= 16;
assigns \nothing;
*/
int test(int a){
int tmp = (a * a) >> 2;
//@ assert assert_tmp: 0 <= tmp <= 64;
//@ assert assert_mult: 0 <= tmp * tmp <= INT_MAX;
return a * a;
}
```

- Run the command :
`frama-c-gui -wp -wp-prover alt-ergo,z3-ce,cvc4-strings-ce -rte issue_shift.c`

All the goals should be proved.

The assertion `assert_mult`

is not verified. Indeed, when a variable is the result of a shift, the multiplication of this variable cannot be bound.

However, if we test with:

```
int tmp = 32;
//@ assert 0 <= tmp * tmp <= INT_MAX
```

The assertion is proved.

I tried to define the following lemma to help the provers but without success.

```
/*@ lemma bound_mult:
\forall int a;
0 <= a <= 64
==> 0 <= a * a <= INT_MAX;
*/
```

Thank you for your answers. I had not thought about this problem of shift on negative values.

As I try to prove a program that used right shifts on negative values, I may use axioms until I find a solution to prove my example or a tactic is added into frama-c.

Yes, the tactic `Logical Shift`

is efficient when using the `-warn-right-shift-negative`

option of Frama-C (in order to explicitly consider negative right shifts as run-time errors).

Nevertheless, Frama-C defines an implementation for C negative right shifts, the same semantics as ACSL negative right shifts. A tactic could be missing for your example, but the development of WP tactics related to implementation defined semantics of C code has a low priority .

In C11, right shifting a value that is negative is implementation defined (see 6.5.7.5 in C11), here `tm`

could either be positive or negative. Note that this is why the tactic `Logical Shift`

generates a goal `positive`

one has to prove that the term is positive.

- Frama-C installation mode:
*Opam* - Frama-C version:
*22.0 (Titanium)* - Plug-in used:
*WP* - OS name:
*Ubuntu* - OS version:
*Ubuntun 20.04.1 LTS*

*Please add specific information deemed relevant with regard to this issue.*

- Get the following C file (issue_shift.c):

```
#include <limits.h>
/*@
requires 0 <= a <= 16;
assigns \nothing;
*/
int test(int a){
int tmp = (a * a) >> 2;
//@ assert assert_tmp: 0 <= tmp <= 64;
//@ assert assert_mult: 0 <= tmp * tmp <= INT_MAX;
return a * a;
}
```

- Run the command :
`frama-c-gui -wp -wp-prover alt-ergo,z3-ce,cvc4-strings-ce -rte issue_shift.c`

All the goals should be proved.

The assertion `assert_mult`

is not verified. Indeed, when a variable is the result of a shift, the multiplication of this variable cannot be bound.

However, if we test with:

```
int tmp = 32;
//@ assert 0 <= tmp * tmp <= INT_MAX
```

The assertion is proved.

I tried to define the following lemma to help the provers but without success.

```
/*@ lemma bound_mult:
\forall int a;
0 <= a <= 64
==> 0 <= a * a <= INT_MAX;
*/
```

Hello again,

I found another example (minimum_example.c) where I cannot prove that the result of a minus operation is bounded when using variables that are computed with shift and multiplication.

```
#include <inttypes.h>
#include <limits.h>
struct Int32Quat {
int32_t qi;
};
#define SQRT_INT_MAX 46340
// 46340 = sqrt(INT_MAX);
/*@ lemma minus_bounded:
\forall int32_t a,b;
INT_MIN / 2 <= a <= INT_MAX / 2
&& INT_MIN / 2 <= b <= INT_MAX / 2
==> INT_MIN <= a - b <= INT_MAX;
*/
/*@
requires \valid(q1);
requires \valid_read(q2) && -SQRT_INT_MAX <= q2->qi <= SQRT_INT_MAX;
requires \valid_read(q3) && -SQRT_INT_MAX <= q3->qi <= SQRT_INT_MAX;
requires \separated(q1, q2, q3);
assigns *q1;
*/
void test_quat(struct Int32Quat *q1, struct Int32Quat *q2, struct Int32Quat *q3){
const int32_t tmp = (q2->qi * q3->qi) >> 2;
//@ assert q2_bounded: INT_MIN / 2 <= q2->qi <= INT_MAX / 2;
//@ assert tmp_bounded: INT_MIN / 2 <= tmp <= INT_MAX / 2;
/*@ assert application_lemma_minus_bounded:
INT_MIN / 2 <= q2->qi <= INT_MAX / 2
&& INT_MIN / 2 <= tmp <= INT_MAX / 2
==> q2->qi - tmp <= INT_MAX;
*/
q1->qi = q2->qi - tmp;
}
```

When running the command `frama-c-gui -wp -wp-prover alt-ergo,z3-ce,cvc4-strings-ce,tip -rte minimum_example.c`

the assertion `application_lemma_minus_bounded`

is not verified. I tried to use the tactic `Logical Shift`

without success. If the shift is replaced by a division, then the assertion is proved.

Maybe I am using frama-c incorrectly or I forgot something.

Thank you in advance.

**François Bobot**
(e6d83995)
*
at
15 Jan 03:38
*

Merge branch 'feature/andre/not-yet-implemented-message' into 'master'

*
... and
13 more commits
*