Project

General

Profile

Bug #9820

Nondeterministic environment model

Added by Pavel Andrianov 3 months ago.

Status:
New
Priority:
Normal
Assignee:
Category:
Environment model
Target version:
-
Start date:
09/16/2019
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

Environment model is constructed nondeterministically: the same scenario functions may have different identifiers (ldv_platform_instance_12 / ldv_platform_instance_11) and the internal variables also may have different identifiers (struct ldv_struct_interrupt_scenario_12 *cf_arg_12 / struct ldv_struct_interrupt_scenario_13 *cf_arg_13). After manual comparison of the files we found that no function is missed, they are just reordered.

I attached two model files, which are generated with the same settings and the same Klever versions.


Files

environment_model2.c (69.3 KB) environment_model2.c The second model Pavel Andrianov, 09/16/2019 01:00 PM
environment_model1.c (69 KB) environment_model1.c The first model Pavel Andrianov, 09/16/2019 01:00 PM

Also available in: Atom PDF