1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
// Copyright (c) 2023 Fotis Koutoulakis for Diffblue Ltd.
/// \file Integration tests for the the interface of the class for verification
/// results produced by various verification engines (classes downstream
/// of goto_verifiert).
#include <libcprover-cpp/api.h>
#include <libcprover-cpp/verification_result.h>
#include <iostream>
#include <memory>
#include <sstream>
#include <string>
#include "../catch/catch.hpp"
SCENARIO(
"When we analyse a model produced from some C code we get back verification "
"results in a structured format",
"[goto-checker][verification-result]")
{
GIVEN("A model with a passing property from C source code")
{
api_sessiont api(api_optionst::create());
api.load_model_from_files({"test2.c"});
WHEN("We run that model past the verification engine")
{
const std::unique_ptr<verification_resultt> results = api.verify_model();
THEN("The verification result should be success")
{
REQUIRE(results->final_result() == verifier_resultt::PASS);
}
THEN(
"We should have access to the property and the property status should "
"be PASS")
{
auto properties = results->get_property_ids();
REQUIRE(properties.size() == 1);
REQUIRE(properties.at(0) == "main.assertion.1");
THEN(
"The property description should be the same as the assertion "
"description in the model")
{
const std::string assertion_description{
"expected success: arr[3] to be 3"};
const std::string results_description =
results->get_property_description(properties.at(0));
REQUIRE(assertion_description == results_description);
}
THEN("The property status should be PASS")
{
const auto property_status =
results->get_property_status(properties.at(0));
REQUIRE(property_status == prop_statust::PASS);
}
}
}
}
GIVEN("A model with a failing property from C source code")
{
api_sessiont api(api_optionst::create());
api.load_model_from_files({"test.c"});
WHEN("We run that model past the verification engine")
{
const auto results = api.verify_model();
THEN("The verification result should be failure")
{
REQUIRE(results->final_result() == verifier_resultt::FAIL);
}
}
}
}
|
