Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Library doesn't have a way to iterate over an integer range with for #2439

Closed
msullivan opened this issue May 24, 2012 · 3 comments
Closed

Library doesn't have a way to iterate over an integer range with for #2439

msullivan opened this issue May 24, 2012 · 3 comments

Comments

@msullivan
Copy link
Contributor

We have a convention for early break from iteration functions; we should update int::range to use it or we should add a new function that does this.
@eholk
Copy link
Contributor

eholk commented May 24, 2012

@pcwalton ran into this issue yesterday too.

@nikomatsakis
Copy link
Contributor

It is my opinion that all iter() style functions are outdated and should be replaced with breakable equivalents.

@brson
Copy link
Contributor

brson commented May 26, 2012

Fixed in 432c6cb

@brson brson closed this as completed May 26, 2012
bors added a commit to rust-lang-ci/rust that referenced this issue Sep 22, 2022
@bors
Auto merge of rust-lang#2439 - RalfJung:ptr-offset-from-unsigned, r=R…
fff4742 
…alfJung

more tests for ptr_offset_from_unsinged
celinval added a commit to celinval/rust-dev that referenced this issue Jun 4, 2024
@celinval
Perform reachability analysis on a per-harness basis (rust-lang#2439)
2a09d79 
Kani compiler used to generate one `goto-program` for all harnesses in one crate. In some cases, this actually had a negative impact on the harness verification time. This was first reported in rust-lang#1659

The main changes were done in the compiler's module `compiler_interface` and the module `project` from the driver. The compiler will now gather all the harnesses beforehand and it will perform reachability + codegen steps for each harness. All files related to a harness `goto-program` will follow the naming convention bellow:
```
<BASE_NAME>_<MANGLED_NAME>.<EXTENSION>
```
This applies to symtab / goto / type_map / restriction files.

The metadata file is still generated once per target crate, and its name is still the same (`<BASE_NAME>.kani-metadata.json`).

On the driver side, the way we process the artifacts have changed. The driver will now read the metadata for each crate, and collect all artifacts based on the symtab goto file that is recorded in the metadata of each harness.

These changes do not apply for `--function`. We still keep all artifacts based on the crate's `<BASE_NAME>` and we have a separate logic to handle that. Fixing this is captured by rust-lang#2129.
celinval added a commit to celinval/rust-dev that referenced this issue Jun 4, 2024
@celinval
Fix symtab json file removal and reduce regression scope (rust-lang#2447
3d05d3f 
)

This fixes a regression introduced in rust-lang#2439 when write symtab json is enabled. We still need to take that into consideration and remove them if needed.

This change also simplifies the write symtab json regression to avoid the out of disk space issue we've been seeing since rust-lang#2439.
celinval added a commit to celinval/rust-dev that referenced this issue Jun 4, 2024
@celinval
Fix regression on concrete playback inplace (rust-lang#2454)
19b7a7d 
This fixes a regression from rust-lang#2439. The compiler should store the location of the function body instead of the declaration. Storing the correct location fixes how concrete playback stores the generated unit test.
celinval added a commit to celinval/rust-dev that referenced this issue Jun 4, 2024
@celinval
Fix MIR dump to emit one MIR per-harness (rust-lang#2556)
3224cbd 
This was a regression introduced by rust-lang#2439. We were still writing the result of the reachability algorithm to the same file for every harness. Thus, we could only see the MIR for the last harness that was processed.

Use the file name that is specific for the harness instead and generate one MIR file per harness like we do with other files generated by kani-compiler.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@eholk @brson @nikomatsakis @msullivan