Attributes such as 'visibility' must be ignored for casting purposes,
to avoid errors with implicit casts.

Merge fixes from Nickel

See merge request frama-c/frama-c!4482

[opam] bump minimal zarith version to 1.9

See merge request frama-c/frama-c!4486

[dev] allow spaces in file names

See merge request frama-c/frama-c!4472

Ivette : Field, label html en Label JSX

See merge request frama-c/frama-c!4479

[Lexer] Handling unsupported types

See merge request frama-c/frama-c!4478

Handling GMP overflow in `power_int_positive_int`

Closes #414

See merge request frama-c/frama-c!4464

[wp] fix prover selection

See merge request frama-c/frama-c!4484

Maxime Jacquemin authored 1 year ago and Andre Maroneze committed 1 year ago

Now, the lexer will produce a nice error message for _Decimal32,
_Decimal64, __int128 and __uint128_t.

[kernel] Cabs2Cil: render error message more precise

Closes #1352

See merge request frama-c/frama-c!4462

Invariant computation for linear filters

See merge request frama-c/frama-c!4438

Maxime Jacquemin authored 1 year ago and David Bühler committed 1 year ago

Modified a test to use the filter's center.

Maxime Jacquemin authored 1 year ago and David Bühler committed 1 year ago

We can now represents filters that are not centered around zero.
The invariant computation now computes bounds for each state dimension.
The module is documented.

Maxime Jacquemin authored 1 year ago and David Bühler committed 1 year ago

Avoiding confusing between physical and structural equality.

Maxime Jacquemin authored 1 year ago and David Bühler committed 1 year ago

- Change Finite.for_each parameters order for a more natural one
- Used Format boxes for some pretty_printers
- Used Finite.for_each instead of a nasty for loop in vector product
- Utilitary function for index computation in matrices
- Simpler computation of the spectral radius

Uses the same convention as Pretty_utils.

Avoids overloading stdlib types.

Maxime Jacquemin authored 1 year ago and David Bühler committed 1 year ago

- The functions `Nat.of_int`, `Nat.of_strictly_positive_int` and
  `Finite.of_int` now returns an option instead of forcing valid
  bounds on their inputs.

- The spectral exponent search is simpler and returns the maximal
  exponent in the given limit that returns a spectral radius lower
  than one.

- A bug has been fixed in the invariant computation. The sum over
  the inputs missed an element.

Maxime Jacquemin authored 1 year ago and David Bühler committed 1 year ago

Under the hood, it's just int. But only valid nat and finite can be
built through the given constructors.

Fix/martin/kernel/restore erased content

Closes #1346

See merge request frama-c/frama-c!4447

- use Alt-Ergo instead of alt-ergo
- resolve ambiguity when several solvers match the provided name

[analysis-scripts] add __int128 to list of unsupported features

See merge request frama-c/frama-c!4469