Skip to content

Commit

Permalink
pythonic refactoring
Browse files Browse the repository at this point in the history
  • Loading branch information
daejunpark committed Sep 9, 2024
1 parent ddb6800 commit 7124320
Showing 1 changed file with 10 additions and 11 deletions.
21 changes: 10 additions & 11 deletions src/halmos/calldata.py
Original file line number Diff line number Diff line change
Expand Up @@ -189,10 +189,8 @@ def encode(self, name: str, typ: Type) -> EncodingResult:
if isinstance(typ, BaseType):

def new_symbol() -> str:
if self.new_symbol_id is None:
return f"p_{name}_{typ.typ}"
else:
return f"p_{name}_{typ.typ}_{self.new_symbol_id():>02}"
id_suffix = f"_{self.new_symbol_id():>02}" if self.new_symbol_id else ""
return f"p_{name}_{typ.typ}{id_suffix}"

# bytes, string
if typ.typ in ["bytes", "string"]:
Expand Down Expand Up @@ -308,10 +306,11 @@ def mk_calldata(


def mk_arrlen(args: HalmosConfig) -> dict[str, int]:
arrlen = {}
if args.array_lengths:
for assign in [x.split("=") for x in args.array_lengths.split(",")]:
name = assign[0].strip()
size = assign[1].strip()
arrlen[name] = int(size)
return arrlen
if not args.array_lengths:
return {}

name_size_pairs = args.array_lengths.split(",")
return {
name.strip(): int(size.strip())
for name, size in [x.split("=") for x in name_size_pairs]
}

0 comments on commit 7124320

Please sign in to comment.