Project

General

Profile

Actions

Feature #8627

closed

Allow forbidding checking final state

Added by Evgeny Novikov over 6 years ago. Updated over 5 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Category:
Environment models
Target version:
Start date:
12/13/2017
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

One more trivial step towards checking C programs different from Linux kernel loadable modules is to have an option to forbid checking the final state. There is some code for which checking final state doesn't have sense while we still can check correctness rules assuming checking the final state for that code.

Actions #1

Updated by Ilja Zakharov about 6 years ago

  • Status changed from New to Resolved

Implemented in 8066-abstract-translator.

Actions #2

Updated by Evgeny Novikov over 5 years ago

  • Status changed from Resolved to Closed

Branch klever-2.0 passed all tests and I merged it to master in 72be796e3 marked as v2.0rc1.

Actions

Also available in: Atom PDF