22160684311

Committed 18 Feb 2026 09:20PM UTC coverage: 88.256% (+1.1%) from 87.142%

Build # 22160684311

Build Type

push

github

Committed by

elazarg

Commit Message

lint

Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

Run Details

78 of 82 new or added lines in 6 files covered. (95.12%)

402 existing lines in 18 files now uncovered.

10731 of 12159 relevant lines covered (88.26%)

837642.51 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

84.21

/src/string_constraints.hpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT

#pragma once

#include <optional>
#include <set>
#include <string>
#include <vector>

#include "arith/linear_constraint.hpp"
#include "arith/variable.hpp"
#include "crab/interval.hpp"
#include "crab/type_encoding.hpp"

namespace prevail {
struct StringInvariant {
    std::optional<std::set<std::string>> maybe_inv{};

    StringInvariant() = default;

    explicit StringInvariant(std::set<std::string> inv) : maybe_inv(std::move(inv)) {}

    StringInvariant(const StringInvariant& inv) = default;
    StringInvariant& operator=(const StringInvariant& inv) = default;
    StringInvariant(StringInvariant&& inv) = default;
    StringInvariant& operator=(StringInvariant&& inv) = default;

    [[nodiscard]]
    bool is_bottom() const {
        return !maybe_inv;
    }
    [[nodiscard]]
    bool empty() const {
        return maybe_inv && maybe_inv->empty();
    }

    static StringInvariant top() { return StringInvariant{{}}; }
    static StringInvariant bottom() { return StringInvariant{}; }

    [[nodiscard]]
    const std::set<std::string>& value() const {
        if (is_bottom()) {
            throw std::runtime_error("cannot iterate bottom");
        }
        return *maybe_inv;
    }

    StringInvariant operator-(const StringInvariant& b) const;
    StringInvariant operator+(const StringInvariant& b) const;

    bool operator==(const StringInvariant& other) const { return maybe_inv == other.maybe_inv; }

    [[nodiscard]]
    bool contains(const std::string& item) const {
        return maybe_inv.value().contains(item);
    }

    friend std::ostream& operator<<(std::ostream&, const StringInvariant& inv);
};

struct TypeSetRestriction {
    Variable var;
    TypeSet types;
};

/// Parsed type equality: v1.type == v2.type.
struct TypeEquality {
    Variable v1;
    Variable v2;
};

struct TypeValueConstraints {
    std::vector<TypeEquality> type_equalities;
    std::vector<TypeSetRestriction> type_restrictions;
    std::vector<LinearConstraint> value_csts;
};

TypeValueConstraints parse_linear_constraints(const std::set<std::string>& constraints,
                                              std::vector<Interval>& numeric_ranges);
} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3
4	#pragma once
5
6	#include <optional>
7	#include <set>
8	#include <string>
9	#include <vector>
10
11	#include "arith/linear_constraint.hpp"
12	#include "arith/variable.hpp"
13	#include "crab/interval.hpp"
14	#include "crab/type_encoding.hpp"
15
16	namespace prevail {
17	struct StringInvariant {	4,486✔
18	std::optional<std::set<std::string>> maybe_inv{};
19
20	StringInvariant() = default;	465✔
21
22	explicit StringInvariant(std::set<std::string> inv) : maybe_inv(std::move(inv)) {}	8,637✔
23
24	StringInvariant(const StringInvariant& inv) = default;	5,003✔
25	StringInvariant& operator=(const StringInvariant& inv) = default;
26	StringInvariant(StringInvariant&& inv) = default;	5,561✔
27	StringInvariant& operator=(StringInvariant&& inv) = default;	94✔
28
29	[[nodiscard]]
30	bool is_bottom() const {	11,184✔
31	return !maybe_inv;	11,184✔
32	}
33	[[nodiscard]]
UNCOV 34	bool empty() const {	×
UNCOV 35	return maybe_inv && maybe_inv->empty();	×
36	}
37
38	static StringInvariant top() { return StringInvariant{{}}; }	1,958✔
39	static StringInvariant bottom() { return StringInvariant{}; }	436✔
40
41	[[nodiscard]]
42	const std::set<std::string>& value() const {	4,144✔
43	if (is_bottom()) {	4,144✔
UNCOV 44	throw std::runtime_error("cannot iterate bottom");	×
45	}
46	return *maybe_inv;	4,144✔
47	}
48
49	StringInvariant operator-(const StringInvariant& b) const;
50	StringInvariant operator+(const StringInvariant& b) const;
51
52	bool operator==(const StringInvariant& other) const { return maybe_inv == other.maybe_inv; }	2,163✔
53
54	[[nodiscard]]
55	bool contains(const std::string& item) const {	4,510✔
56	return maybe_inv.value().contains(item);	4,510✔
57	}
58
59	friend std::ostream& operator<<(std::ostream&, const StringInvariant& inv);
60	};
61
62	struct TypeSetRestriction {
63	Variable var;
64	TypeSet types;
65	};
66
67	/// Parsed type equality: v1.type == v2.type.
68	struct TypeEquality {
69	Variable v1;
70	Variable v2;
71	};
72
73	struct TypeValueConstraints {
74	std::vector<TypeEquality> type_equalities;
75	std::vector<TypeSetRestriction> type_restrictions;
76	std::vector<LinearConstraint> value_csts;
77	};
78
79	TypeValueConstraints parse_linear_constraints(const std::set<std::string>& constraints,
80	std::vector<Interval>& numeric_ranges);
81	} // namespace prevail

Alan-Jowett / ebpf-verifier / 22160684311

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous