ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
ld_ir_builder.h
Go to the documentation of this file.
1#pragma once
2
5
6// Lowers a type-checked LdAst into LdIR by applying SOS rule assignments.
8{
9public:
10 LdIR build(const LdAst &ast);
11
12private:
13 LdIRNode lower_element(const RungElement &elem);
14 LdIRRung lower_rung(const RungNode &rung);
15};
Definition ld_ir_builder.h:8
LdIR build(const LdAst &ast)
Definition ld_ir_builder.cpp:106
Definition ld_ast.h:256
Definition ld_ir.h:30
Definition ld_ir.h:70
Definition ld_ir.h:91
Definition ld_ast.h:141
Definition ld_ast.h:153