Project

General

Profile

Actions
Copy link

Bug #9820

closed

Nondeterministic environment model

Added by Pavel Andrianov about 5 years ago. Updated over 4 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Ilja Zakharov
Category:
Environment models
Target version:
3.0
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

Download all 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
Actions
Copy link

Also available in: Atom PDF