Skip to content

Commit

Permalink
Formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
JustusAdam committed Nov 29, 2023
1 parent 904ef0e commit 981a465
Showing 1 changed file with 17 additions and 7 deletions.
24 changes: 17 additions & 7 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
Original file line number Diff line number Diff line change
Expand Up @@ -302,11 +302,16 @@ impl CodegenBackend for GotocCodegenBackend {
.unwrap();
let Ok(contract_metadata) =
contract_metadata_for_harness(tcx, harness.def_id())
else {
continue;
};
let (gcx, items, contract_info) =
self.codegen_items(tcx, &[harness], model_path, &results.machine_model, contract_metadata);
else {
continue;
};
let (gcx, items, contract_info) = self.codegen_items(
tcx,
&[harness],
model_path,
&results.machine_model,
contract_metadata,
);
results.extend(gcx, items, None);
if let Some(assigns_contract) = contract_info {
self.contract_channel
Expand All @@ -333,8 +338,13 @@ impl CodegenBackend for GotocCodegenBackend {
// We will be able to remove this once we optimize all calls to CBMC utilities.
// https://github.com/model-checking/kani/issues/1971
let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
let (gcx, items, contract_info) =
self.codegen_items(tcx, &harnesses, &model_path, &results.machine_model, Default::default());
let (gcx, items, contract_info) = self.codegen_items(
tcx,
&harnesses,
&model_path,
&results.machine_model,
Default::default(),
);
results.extend(gcx, items, None);

assert!(contract_info.is_none());
Expand Down

0 comments on commit 981a465

Please sign in to comment.