[kernel] some fixes related to default spec

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

David Bühler authored 3 years ago and Patrick Baudin committed 2 years ago

With the automatic generation of `terminates` clauses, there is no empty
function contract. Instead, we detect function specification without any
assigns clause, which is unsound for the Eva analysis.

[Install] frama-c-test.sh

Closes #1154

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

Remove functions from `Extlib`

Closes #1091

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

[e acsl] restore libc test suite

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

[ptests] adds universe deps to @disabled_ptests targets

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

[Doc] devman: update 4.1 to 4.3

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

[Ptests] fixes EXECNOW with unconsumed BIN and without LOG

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

[tests] remove empty oracles

Closes e-acsl#205

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

[ptests] adds -config option

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

Make release process almost entirely automatic

Closes #512

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

[ptests] adds @disabled_ptests targets

Closes #1157

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